package alloy.symm;


import java.util.Collections;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;

import alloy.ast.CompOp;
import alloy.ast.ElemFormula;
import alloy.ast.Expr;
import alloy.ast.Leaf;
import alloy.ast.LeafId;
import alloy.transl.ASTInfo;
import alloy.util.Util;

/**
 * For each unary relation (set), find other relations constrained to contain this relation.
 * I.e. for each unary relation u finds relations v such that the constraint "u in v" is conjoined at the root of the AST.
 * @see SBM_DisjSingletons
 */
class SubsetDetector_V extends TopLevelConjVisitor {
    /**
     * Maps {@link LeafId} of a unary relation u to a Set Leaf ids of unary relations v for which "u in v" is a top-level fact.
     */
    private Map /* LeafId->Set[LeafId] */ _subset2supersets = Util.makeMap();

    private ASTInfo _astInfo;

    /////////////
    // Methods //
    /////////////

	SubsetDetector_V(ASTInfo astInfo_) { _astInfo = astInfo_; }

    /**
     * For a top-level conjunct of the form "u in v" record that u is contained in v.
     */
	public void visit(ElemFormula elemFormula_) {
	    // if it's "u !in v" the ignore it
	    if (elemFormula_.getOp().isNegated()) return;
	    
	    Expr left = elemFormula_.getLeft();
	    Expr right = elemFormula_.getRight();
	    
	    if (left.getType().toRelationType().numBasicTypes() != 1 ||
		right.getType().toRelationType().numBasicTypes() != 1)
		return;

	    
	    if (left instanceof Leaf && right instanceof Leaf) {
		LeafId leftId = ((Leaf)left).getLeafId();
		LeafId rightId = ((Leaf)right).getLeafId();

		if (!_astInfo.getRelations().contains(leftId) ||
		    !_astInfo.getRelations().contains(rightId))
		    return;
		
		_recordSubset(leftId, rightId);
		if (elemFormula_.getOp().equals(CompOp.EQUALS))
		    _recordSubset(rightId, leftId);
	    }
	}

    /** Record that left is a subset of right */
    private void _recordSubset(LeafId left_, LeafId right_) {
	Set /* of LeafId */ supersetsOfLeft = (Set)_subset2supersets.get(left_);
	if (supersetsOfLeft == null)
	    _subset2supersets.put(left_, supersetsOfLeft = Util.makeSet());
	supersetsOfLeft.add(right_);
    }

    /** Compute a transitive closure of the subset relation: if u in v and v in w then record that u in w */
    private void _computeTransitiveClosure() {
	boolean arcsAdded;

	do {
	    arcsAdded = false;
	    for (Iterator leftIter = _subset2supersets.keySet().iterator(); leftIter.hasNext();) {
		LeafId left = (LeafId)leftIter.next();
		Set /* of LeafId */ rights = (Set)_subset2supersets.get(left);
		for (Iterator rightIter = rights.iterator(); rightIter.hasNext();) {
		    LeafId right = (LeafId)rightIter.next();
		    Set /* of LeafId */ rightSupersets = (Set)_subset2supersets.get(right);
		    if (rightSupersets != null) {
			for (Iterator rightSupersetIter = rightSupersets.iterator(); rightSupersetIter.hasNext();) {
			    LeafId rightSuperset = (LeafId)rightSupersetIter.next();
			    if (rights.add(rightSuperset))
				arcsAdded = true;
			}
		    }
		}
	    }
	} while (arcsAdded);
    }

    /** Return the Set of supersets of a given unary relation */
    Set /* of LeafId */ getSupersets(LeafId id_) {
	Set /* of LeafId */ supersets = (Set)_subset2supersets.get(id_);
	return supersets!=null ? supersets : Collections.EMPTY_SET;
    }
}
